COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 standard inst
C00005 00003	Notes on Gabriel matcher match.>[aid,rpg].
C00008 ENDMK
C⊗;
;;; standard inst

(defun sublis (p a)
       (if (atom p)
	   ((lambda (z) (if (null z) p (cdr z))) (assoc p a))
	   (cons (sublis (car p) a) (sublis (cdr p) a))))

(DEFUN INST (PAT EXPR A)
       (COND ((EQ A 'NO) 'NO)
	     ((ISVAR PAT) ((LAMBDA (Z) (COND ((NULL Z) (CONS (CONS PAT EXPR) A))
					     ((EQ (CDR Z) EXPR) A)
					     (T 'NO)))
			   (ASSOC PAT A)))
	     ((ATOM PAT) (COND ((EQ PAT EXPR) A)
			       (T 'NO)))
	     ((ATOM EXPR) 'NO)
	     (T (INST (CDR PAT) (CDR EXPR) (INST (CAR PAT) (CAR EXPR) A)))))

;;;inst using throw and catch

(DEFUN ISVAR (X) (MEMBER X '(X X0 X1 X2 Y Y0 Y1 Y2 Z Z0 Z1 Z2 U U0 U1 U2
V V0 V1 V2 W W0 W1 W2)))

(defun instth (pat exp a) (catch (instth1 pat exp a)))

(defun instth1 (pat exp a)
	(if	(isvar pat)
		((lambda (w)
			(if	(null w)
				(cons (cons pat exp) a)
				(equal (cdr w) exp)
				a
				(throw 'no)
			))
		 (assoc pat a))
		(atom pat)
		(if (eq pat exp) a (throw 'no))
		(atom exp)
		(throw 'no)
		(instth1 (cdr pat) (cdr exp) (instth1 (car pat) (car exp) a))
	)
)

;;;inst using predicates

(defun instp (pat exp a) (if (isvar pat) ((lambda (w)
(or (and (null w) (cons (cons pat exp) a))
    (and (eq (cdr w) exp) a)))       (assoc pat a))
(atom pat) (and (eq pat exp) a)
(and (not (atom exp)) (instp (cdr pat) (cdr exp) (instp (car pat) (car exp) a)))
))

;;;a version of inst that sets variables

(DEFUN MATCH (EXPR PATTERN)
(PROG (W)
(SETQ W (INST EXPR PATTERN NIL))
LLLL
(COND ((ATOM W) (RETURN W)))
(SET (CAAR W) (CDAR W))
(SETQ W (CDR W))
(GO LLLL)
))

;;;list of functions

(setq instfns '(inst instth instth1 isvar instp match))
Notes on Gabriel matcher match.>[aid,rpg].

	Works fine but

1. Not clear how to use it to program a simplifier that simplifies
internally as well as on the outside.  Needs a special corresponding
sublis or multiple subst.  Its use doesn't gain much in the step
of differentiating a product.

2. Won't work if reserved words or variables of its form occur
in the expression being matched or as constants in the pattern.
I guess it will; they need only be quoted.  The question is whether
the matcher is self-applicable, and I guess it is to a reasonable
extent.  More generally, the patterns should be friendly to being
generated by LISP program.  Gabriel's is better than Masinter's
in that respect.

3. However, Masinter's has a writeup in the Interlisp manual, and
Gabriel's has no writeup except in the same file as the program.

4. Biggest problem for me is proving correctness.  That inst and
sublis are inverses is an exercise.  How even to formulate correctness
of programs using SET is problematical.  No problem in Elephant.
For an ordinary variable x, Elephant has a function x(t).  We can
write value('x,t) = x(t), and there is no difference between
proving something about x(t) and proving the same thing about
value('x,t).  SETs are treated by working with value(v(t),t)
with v(t1) = 'x and v(t2) = 'y, etc.  How this works in pattern
matching is another question.